es:ES, e1, e2:E, P:({e:E| loc(e) = loc(e1)  Id }Prop).
loc(e2) = loc(e1)  Id  e@loc(e1). Dec(P(e))  Dec(e[e1,e2).P(e)) 

latex

Definitions	x:A. B(x), Prop, P  Q, x(s), e[e1,e2).P(e), t  T, x. t(x), e@i. P(e), Dec(P), P  Q, {T}, (e <loc e'), P & Q, P  Q, e<e'. P(e)
Lemmas	alle-at wf, decidable wf, es-E wf, Id wf, es-loc wf, event system wf, decidable alle-lt, es-le wf, decidable implies better, decidable es-le, not wf, es-locl wf, es-le-loc, es-loc-pred, es-locl-iff